\begin{tabbing}
star{-}append($T$; $P$; $Q$)($L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it LL}$:$T$ List List\+
\\[0ex]$\exists$\=${\it L'}$:$T$ List\+
\\[0ex](l\_all(${\it LL}$; ($T$ List); $X$.($P$($X$))) $\wedge$ ($Q$(${\it L'}$)) $\wedge$ ($L$ = append(concat(${\it LL}$); ${\it L'}$) $\in$ ($T$ List)))
\-\-
\end{tabbing}